Technique: Programs are Proofs

"In 1934 Curry observed that the types of combinatory logic can be seen as axioms of intuitionistic logic. In 1969 Howard observed that natural deduction from proof theory forms a model for the lambda calculus. More informally, the return type of a function is analogous to a logical theorem, subject to hypotheses corresponding to the types of the argument; and that the program to compute that function is analogous to a proof of that theorem. This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run." https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

However, history didnt stop 1969. Up until this day exciting things can be explained and discovered by exploiting proofs that can run and give results, such as:

• Intrinsic Proofs
• Well-typed & Well-scoped interpreters
• Parametricity translation
• Logical Relations
• Type-and-Effect System
• Type-and-Coeffect System

Some recent papers we find interesting are:

• A correct-by-construction conversion from lambda calculus to combinatory logic
• On the Versatility of Open Logical Relations
• Differential Logical Relations. Part II: Increments and Derivatives
• Homotopical Patch Theory